theorem other other

`then`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

 294theorem then says that any other cost function `κ'` agreeing with
 295`κ` on `α` and on the chosen indecomposable inconsistent
 296configurations agrees with `κ` everywhere expressible as
 297independent joins of those generators.
 298-/

depends on (12)

Lean names referenced from this declaration's body.

of in IndisputableMonolith.Astrophysics.NucleosynthesisTiers decl_use
independent in IndisputableMonolith.ClassicalBridge.Fluids.LNALSemantics decl_use
of in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization decl_use
cost in IndisputableMonolith.Foundation.MultiplicativeRecognizerL4 decl_use
cost in IndisputableMonolith.Foundation.ObserverForcing decl_use
of in IndisputableMonolith.Foundation.PhiForcingDerived decl_use
independent in IndisputableMonolith.Foundation.RSCoupledAxis decl_use
as in IndisputableMonolith.Foundation.SimplicialLedger.ContinuumBridge decl_use
of in IndisputableMonolith.Foundation.SpectralEmergence decl_use
of in IndisputableMonolith.Information.PhysicsComplexityStructure decl_use
and in IndisputableMonolith.NumberTheory.CirclePhaseLift decl_use
that in IndisputableMonolith.NumberTheory.PhiLadderLattice decl_use