Numeral MIP Bridge

@cite{fox-hackl-2006} @cite{kennedy-2015}

Surfaces the maximal informativity theorems from Theories/Semantics/Entailment/Extremum.lean at the Phenomena level, connecting numeral semantics (the named *Meaning functions) to the HasMaxInf / IsMaxInf infrastructure and the @cite{fox-hackl-2006} density predictions.

Bridge Structure

The named numeral meanings (atLeastMeaning, moreThanMeaning, ...) are abbrevs over Core.Scale.{atLeastDeg, moreThanDeg, ...} id in Theories/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 Phenomena.Numerals.MIPBridge.atLeast_has_maxInf_at_3 : Semantics.Entailment.Extremum.HasMaxInf (Core.Scale.atLeastDeg id) 3

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

theorem Phenomena.Numerals.MIPBridge.atLeast_has_maxInf_general (n : ℕ) : Semantics.Entailment.Extremum.HasMaxInf (Core.Scale.atLeastDeg id) n

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

theorem Phenomena.Numerals.MIPBridge.moreThan_has_maxInf_nat : Semantics.Entailment.Extremum.HasMaxInf (Core.Scale.moreThanDeg 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 Phenomena.Numerals.MIPBridge.mip_derives_exact (m n : ℕ) : Semantics.Entailment.Extremum.IsMaxInf (Core.Scale.atLeastDeg 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: @cite{kennedy-2015}'s "de-Fregean" type-shift IS the MIP.

structure Phenomena.Numerals.MIPBridge.FoxHacklAsymmetry : Type

The @cite{fox-hackl-2006} 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

@[implicit_reducible]

instance Phenomena.Numerals.MIPBridge.instReprFoxHacklAsymmetry : Repr FoxHacklAsymmetry

Equations

• Phenomena.Numerals.MIPBridge.instReprFoxHacklAsymmetry = { reprPrec := Phenomena.Numerals.MIPBridge.instReprFoxHacklAsymmetry.repr }

def Phenomena.Numerals.MIPBridge.instReprFoxHacklAsymmetry.repr : FoxHacklAsymmetry → ℕ → Std.Format

Equations

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

def Phenomena.Numerals.MIPBridge.foxHackl_asymmetry_data : FoxHacklAsymmetry

The asymmetry prediction, verified against the algebra.

Equations

• Phenomena.Numerals.MIPBridge.foxHackl_asymmetry_data = { atLeast_always := true, moreThan_discrete := true, moreThan_dense := false }

theorem Phenomena.Numerals.MIPBridge.foxHackl_atLeast_verified : foxHackl_asymmetry_data.atLeast_always = true

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

theorem Phenomena.Numerals.MIPBridge.kennedy_numeral_licensed {W : Type u_1} (μ : W → ℕ) : (Core.Scale.DirectedMeasure.numeral μ).licensed = true

Kennedy numeral domains are always licensed (closed scale).