Numeral MIP Bridge

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

Surfaces the abstract Core.Scale maximal informativity theorems at the Phenomena level, connecting numeral semantics (maxMeaning) to the HasMaxInf / IsMaxInf infrastructure and the @cite{fox-hackl-2006} density predictions.

Bridge Structure

1. maxMeaning ↔ atLeastDeg: maxMeaning.ge is the decidable restriction of atLeastDeg id, proved via maxMeaning_ge_iff_atLeastDeg.

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

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

4. 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_3_is_atLeastDeg (n : ℕ) : Semantics.Lexical.Numeral.maxMeaning Semantics.Lexical.Numeral.OrderingRel.ge 3 n = true ↔ Core.Scale.atLeastDeg id 3 n

maxMeaning.ge (numeral "at least") matches atLeastDeg id.

theorem Phenomena.Numerals.MIPBridge.moreThan_3_is_moreThanDeg (n : ℕ) : Semantics.Lexical.Numeral.maxMeaning Semantics.Lexical.Numeral.OrderingRel.gt 3 n = true ↔ Core.Scale.moreThanDeg id 3 n

maxMeaning.gt (numeral "more than") matches moreThanDeg id.

theorem Phenomena.Numerals.MIPBridge.atLeast_has_maxInf_at_3 : Core.Scale.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 : ℕ) : Core.Scale.HasMaxInf (Core.Scale.atLeastDeg id) n

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

theorem Phenomena.Numerals.MIPBridge.moreThan_has_maxInf_nat : Core.Scale.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 : ℕ) : Core.Scale.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

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.kennedyNumeral μ).licensed = true

Kennedy numeral domains are always licensed (closed scale).