module module high

`IndisputableMonolith.Gravity.SevenGaps.Gap2FugacityPostingGluing`

Defines unit sector fugacity: the size function equals one at each of the three atoms (vertices, edges, triangles). That triple is the hypothesis of the gluing derivation's unit-fugacity Gibbs lemma and is premise flag 8 of the full-theory ledger. The module equates size-blind Gibbs weights to class mass mu at the atoms, introduces character costs on the gluing-residue family, and records their equivariance and history-cost identities. Downstream fugacity-elimination and gauge-counting census modules import it.

claimUnit sector fugacity means the size function $f$ satisfies $f(v)=f(e)=f(t)=1$ at the three atoms. Equivalently, the size-blind Gibbs weight posts class mass $\mu$ at those atoms, and the three sector fugacities collapse. Character costs on the gluing-residue family $z_V,z_E,z_T$ are size-blind letter costs whose history cost equals the character cost.

background

Gap 2 in the gravity ledger concerns when a posting-layer letter cost posts the physical class mass $\mu$ without injecting extra Boltzmann factors. The upstream non-equivariant posting module closes the equivariant route: an equivariant letter cost posts $\mu$ exactly when its numerator $\exp(-\mathrm{historyCost})$ is identically one. It leaves open the non-equivariant class (e.g. vertex-index costs).

This module isolates the unit-fugacity condition on the size function at the three atoms. That condition is exactly the hypothesis triple of the carrier-shuffle Gibbs lemma in the gluing derivation, and it is flag 8 of the full-theory ledger. Sibling definitions introduce size-blind Gibbs weights, equate them to class mass $\mu$ at the atoms, and define character costs on the gluing-residue family together with kind-rate and equivariance facts.

The local setting is Recognition Science gravity: after the erasure Jacobian, sector fugacities must collapse so the measure substrate reduces to gauge counting $\nu=1/|\mathrm{Aut}|$.

proof idea

Definition-and-equivalence module, not a single theorem proof. It packages UnitFugacity as the size-function-one-at-atoms predicate, then proves a chain of iff lemmas: Gibbs weight equals Gibbs size; class mass of a size weight equals $\mu$ iff unit fugacity; Gibbs size is one at atom sizes; unit fugacity iff $\mu$ at the atoms and iff normalized at the atoms. Character-cost definitions and lemmas (kind rates, kind-only, equivariance, history-cost identity) supply the gluing-residue family used later for elimination. Argument shape is algebraic rewriting of Boltzmann numerators and size weights at three fixed atoms.

why it matters in Recognition Science

Feeds two parents. Gap2FugacityElimination (lane C17) uses unit fugacity as the forced conclusion after the C4 erasure Jacobian: any letter cost whose posted class mass equals $\mu$ at the three atoms and is representable there by a size-blind weight forces unit fugacity, collapsing the three sector fugacities; on the character-size family this is exact. GaugeCountingInevitableReasons imports the same package when listing necessary reasons that richer posting-layer structure forces the gauge-counting principle for physical class mass.

In the Recognition framework this is the concrete realization of ledger flag 8: without unit fugacity at the atoms, the measure substrate does not reduce to $\nu=1/|\mathrm{Aut}|$, and the Gap-2 gluing derivation cannot discharge its Gibbs hypothesis. It sits between non-equivariant posting resolution and full fugacity elimination.

scope and limits

Does not prove that every physical letter cost is unit-fugacity; only defines the condition and its atom-level equivalences.
Does not close non-equivariant posting costs; that remains upstream witness territory.
Does not derive the erasure Jacobian or force mu from first principles.
Does not establish the gauge-counting principle; only supplies a premise used in its reason census.
Does not address continuum or non-atomic size functions outside the three atoms.

used by (2)

From the project-wide theorem graph. These declarations reference this one in their body.

IndisputableMonolith.Gravity.SevenGaps.Gap2FugacityElimination module_import
IndisputableMonolith.Gravity.SevenGaps.GaugeCountingInevitableReasons module_import

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Gravity.SevenGaps.Gap2NonEquivariantPosting module_import

declarations in this module (40)

def UnitFugacity L126
theorem gibbsWeight_eq_gibbsSize L131
theorem classMass_sizeWeight_eq_mu_iff L141
theorem gibbsSize_eq_one_at_atom_sizes L155
theorem gibbsSize_unitFugacity L164
theorem unitFugacity_iff_mu_at_atoms L181
theorem unitFugacity_iff_normalizedAtTheAtoms L219
def characterCost L244
theorem characterCost_kindRates L250
theorem characterCost_kindOnly L255
theorem characterCost_equivariant L261
theorem historyCost_characterCost L265
theorem exp_log_mul_nat L272
theorem exp_neg_historyCost_characterCost L284
theorem postedWeight_characterCost L301
theorem postedWeight_characterCost_eq L307
theorem postedWeight_characterCost_sizeBlind L314
theorem characterSize_atom_vertex L320
theorem characterSize_atom_edge L324
theorem characterSize_atom_tet L328
theorem unitFugacity_characterSize_iff L334
theorem characterSize_gluesAt L350
theorem characterCost_countermodel L362
theorem gluing_and_posting_do_not_force_unit_fugacity L389
theorem characterCost_posts_mu_iff L410
theorem posts_mu_at_atoms_forces_unit_fugacity L437
theorem posts_mu_forces_gibbsSize L448
theorem gluing_hypothesis_is_idle L467
theorem postedWeight_tiltedCost_not_sizeWeight L488
theorem tiltedCost_classMass_eq_classMass_gibbsSize L499
theorem tiltedCost_classMass_glues_with_unit_fugacity L514
theorem no_posting_countermodel_with_nonunit_fugacity L534
theorem fugacity_posting_gluing_verdict L565
structure Index L591
def index L613
theorem index_premise_is_mu_at_atoms L623
theorem index_fugacity_free L624
theorem index_no_countermodel L625
theorem index_premise_not_derived L626
theorem index_not_shown_underivable L627