Numeral MIP Bridge

[FH06b] [Ken15]

Surfaces the maximal informativity theorems from Semantics/Entailment/Extremum.lean at the Studies level, connecting numeral semantics (the named *Meaning functions) to the HasMaxInf / IsMaxInf infrastructure and the [FH06b] density predictions.

Bridge Structure

The named numeral meanings (atLeastMeaning, moreThanMeaning, ...) are defs over Core.Order.Comparison.{ge, gt, ...}.over id in Semantics/Numerals/Basic.lean §2 — the connection holds by construction, no bridge lemma needed.

1. HasMaxInf for "at least": atLeast_hasMaxInf gives the existence of a maximally informative element for any "at least" degree property.

2. Discrete "more than": on ℕ, moreThan_nat_hasMaxInf shows "more than" also has max⊨, recovering the Fox & Hackl asymmetry.

3. MIP derives exact meaning: isMaxInf_atLeast_iff_eq proves max⊨ of "at least n" at world w iff μ(w) = n.

theorem FoxHackl2006Numerals.atLeast_has_maxInf_at_3 : Entailment.HasMaxInf (Core.Order.Comparison.ge.over id) 3

"At least n" always has a maximally informative element. Instantiated on ℕ with id as the measure function.

theorem FoxHackl2006Numerals.atLeast_has_maxInf_general (n : ℕ) : Entailment.HasMaxInf (Core.Order.Comparison.ge.over id) n

Generalized: "at least n" has max⊨ at every world n.

theorem FoxHackl2006Numerals.moreThan_has_maxInf_nat : Entailment.HasMaxInf (Core.Order.Comparison.gt.over id) 3

On ℕ, "more than 2" has a maximally informative element at world 3. This is the discrete rescue: ℕ's successor structure collapses "more than n" to "at least n+1", which has max⊨.

Contrast with moreThan_noMaxInf on dense scales: no rescue there.

theorem FoxHackl2006Numerals.moreThan_exhChain_crash (c maxD : ℚ) : ¬Exhaustification.exhChain (fun (x d : ℚ) => x < d) c maxD

The dense half of the asymmetry as chain-exhaustification: on ℚ the stronger more than alternatives have no next member, so exhaustifying more than c against its own scale is unsatisfiable — Exhaustification.exhChain_not_of_dense at the UDM scale. On ℕ the next member exists and exhaustification returns 'exactly' instead (Semantics.Numerals.exhNumeral_eq_exhChain).

theorem FoxHackl2006Numerals.mip_derives_exact (m n : ℕ) : Entailment.IsMaxInf (Core.Order.Comparison.ge.over id) m n ↔ n = m

max⊨ of "at least n" at world w ↔ the true value equals n. This is the MIP derivation of exact meaning from lower-bound semantics: [Ken15]'s "de-Fregean" type-shift IS the MIP.

structure FoxHackl2006Numerals.FoxHacklAsymmetry : Type

The [FH06b] implicature asymmetry prediction:

• "at least n" generates scalar implicatures (HasMaxInf) ✓
• "more than n" on dense scales does NOT (moreThan_noMaxInf)
• "more than n" on ℕ DOES (discrete rescue)

This structure records the prediction for bridge verification.

• atLeast_always : Bool

  "At least" has max⊨ on any scale

• moreThan_discrete : Bool

  "More than" has max⊨ on ℕ (discrete)

• moreThan_dense : Bool

  "More than" has max⊨ on dense scales

def FoxHackl2006Numerals.instReprFoxHacklAsymmetry.repr : FoxHacklAsymmetry → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance FoxHackl2006Numerals.instReprFoxHacklAsymmetry : Repr FoxHacklAsymmetry

Equations

• FoxHackl2006Numerals.instReprFoxHacklAsymmetry = { reprPrec := FoxHackl2006Numerals.instReprFoxHacklAsymmetry.repr }

def FoxHackl2006Numerals.foxHackl_asymmetry_data : FoxHacklAsymmetry

The asymmetry prediction, verified against the algebra.

Equations

• FoxHackl2006Numerals.foxHackl_asymmetry_data = { atLeast_always := true, moreThan_discrete := true, moreThan_dense := false }

theorem FoxHackl2006Numerals.foxHackl_atLeast_verified : foxHackl_asymmetry_data.atLeast_always = true

The "at least" part: always has max⊨ (any scale, any world).

theorem FoxHackl2006Numerals.kennedy_numeral_licensed {W : Type u_1} (μ : W → ℕ) : (Degree.DirectedMeasure.numeral μ).IsLicensed

Kennedy numeral domains are always licensed (closed scale).

theorem FoxHackl2006Numerals.kennedy_numeral_isMaxInf {W : Type u_1} (μ : W → ℕ) (m : ℕ) (w : W) (hSurj : Function.Surjective μ) : Entailment.IsMaxInf (Degree.DirectedMeasure.numeral μ).degreeProperty m w ↔ μ w = m

[Ken15]'s de-Fregean type-shift at the DirectedMeasure constructor level: the maximally informative degree of a numeral domain's derived property is the true cardinality — the bundled form of isMaxInf_atLeast_iff_eq.