recognition explainers

500 ready

• asubIter

  def in IndisputableMonolith.Foundation.SingularSubdivision

  def 2026-08-13

• leq

  def in IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.IntegerRational

  def 2026-08-13

• sub_not_balanced_zero_iff_of_balanced_right

  theorem in IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.IntegerOrder

  theorem 2026-08-13

• IndisputableMonolith.Physics.ElectronMass.Defs

  module guide in IndisputableMonolith.Physics.ElectronMass.Defs

  module 2026-08-13

• mul_balanced_zero_of_balanced_zero_right

  theorem in IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.IntegerOrder

  theorem 2026-08-13

• compose

  def in IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.ValidComparison

  def 2026-08-13

• zero_eq

  theorem in IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.IntegerRational

  theorem 2026-08-13

• continuous_arcFun

  lemma in IndisputableMonolith.Foundation.LinkingVanishingHighDim

  lemma 2026-08-13

• windingChainMap

  def in IndisputableMonolith.Foundation.CircleWindingChain

  def 2026-08-13

• DirectedCycleFreeTerm

  structure in IndisputableMonolith.Foundation.CircleWindingChain

  structure 2026-08-13

• eval_ground_step

  theorem in IndisputableMonolith.Foundation.SeamClosure.Reference

  theorem 2026-08-13

• IsProjector

  def in IndisputableMonolith.Foundation.CostProjectorGolden

  def 2026-08-13

• zero_crossEq_recip_zero

  theorem in IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.IntegerOrder

  theorem 2026-08-13

• squareBoundaryPair

  def in IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.CubicalChainComplex

  def 2026-08-13

• singularOneChainFree

  abbrev in IndisputableMonolith.Foundation.CircleWindingChain

  abbrev 2026-08-13

• zero

  def in IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.IntegerRational

  def 2026-08-13

• gen_pushSimplex_comp_tOp

  lemma in IndisputableMonolith.Foundation.SingularSubdivision

  lemma 2026-08-13

• faceBoundaryBoundary

  def in IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.MultiDistinctionGeometry

  def 2026-08-13

• balanced_negate_iff

  theorem in IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.IntegerOrder

  theorem 2026-08-13

• sub_balanced_zero_iff_of_balanced_left

  theorem in IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.IntegerOrder

  theorem 2026-08-13

• abs

  def in IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.IntegerRational

  def 2026-08-13

• generated_all

  theorem in IndisputableMonolith.Foundation.SeamClosure.Reference

  theorem 2026-08-13

• lt

  def in IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.IntegerRational

  def 2026-08-13

• canonicalThreshold

  def in IndisputableMonolith.Foundation.RS_Forcing_Chain_Module_002

  def 2026-08-13

• mul_not_balanced_zero_iff

  theorem in IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.IntegerOrder

  theorem 2026-08-13

• domainCost

  def in IndisputableMonolith.Foundation.RS_Forcing_Chain_Module_009

  def 2026-08-13

• nonnegFlag_zero_sub

  theorem in IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.IntegerOrder

  theorem 2026-08-13

• balanced_add_left_iff

  theorem in IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.IntegerOrder

  theorem 2026-08-13

• sameSetoid

  def in IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.Quotient

  def 2026-08-13

• ForcedAfterTightening

  def in IndisputableMonolith.Foundation.MaximalForcing.AdmissibleRealization

  def 2026-08-13

• IndisputableMonolith.Foundation.SIBridgeClosure

  module guide in IndisputableMonolith.Foundation.SIBridgeClosure

  module 2026-08-13

• abs_le_trans

  theorem in IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.IntegerOrder

  theorem 2026-08-13

• balanced_sub_inputs_iff_of_balanced

  theorem in IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.IntegerOrder

  theorem 2026-08-13

• domainCost

  def in IndisputableMonolith.Foundation.RS_Forcing_Chain_Module_006

  def 2026-08-13

• forced_difference_neg_swap

  theorem in IndisputableMonolith.Foundation.UniversalForcing.ForcedIntegers

  theorem 2026-08-13

• nonnegFlag_sub_zero

  theorem in IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.IntegerOrder

  theorem 2026-08-13

• primitiveLedgerPosting_forces_rightPostedAdditive

  theorem in IndisputableMonolith.Foundation.LedgerToFactorization

  theorem 2026-08-13

• abs_mul_eq_zero_iff_balanced_zero

  theorem in IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.IntegerOrder

  theorem 2026-08-13

• neutralRegister

  def in IndisputableMonolith.Foundation.RecognitionOperator

  def 2026-08-13

• seedClosureEquiv_self_iff_seed_size_law

  theorem in IndisputableMonolith.Foundation.UnifiedForcingChain

  theorem 2026-08-13

• circleH1Z_is_mathlib_singular_homology

  theorem in IndisputableMonolith.Foundation.MathlibCohomologyBridge

  theorem 2026-08-13

• OperatorCore_Forced

  structure in IndisputableMonolith.Foundation.UnifiedForcingChain

  structure 2026-08-13

• incl01_apply_coord

  lemma in IndisputableMonolith.Foundation.UnknotComplementRetract

  lemma 2026-08-13

• IndisputableMonolith.Gravity.HawkingTemperatureSI

  module guide in IndisputableMonolith.Gravity.HawkingTemperatureSI

  module 2026-08-13

• cyclicShiftIter_smul

  lemma in IndisputableMonolith.Foundation.RecognitionOperator

  lemma 2026-08-13

• nonnegativeWork_support_disjoint

  theorem in IndisputableMonolith.Foundation.UnifiedForcingChain

  theorem 2026-08-13

• t6_to_canonical_mass_ladder_bridge_holds

  theorem in IndisputableMonolith.Foundation.UnifiedForcingChain

  theorem 2026-08-13

• deltaForced_int

  theorem in IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.DeltaForced

  theorem 2026-08-13

• canonical_realized_closed_scale_normal_form_equivalence

  theorem in IndisputableMonolith.Foundation.UnifiedForcingChain

  theorem 2026-08-13

• tightening_does_work

  theorem in IndisputableMonolith.Foundation.MaximalForcing.AdmissibleRealization

  theorem 2026-08-13

• canonicalMassExponent

  def in IndisputableMonolith.Foundation.UnifiedForcingChain

  def 2026-08-13

• recip_num_zero_cmp_of_not_balanced_zero

  theorem in IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.IntegerOrder

  theorem 2026-08-13

• cmp_of_sub_left_input_of_balanced

  theorem in IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.IntegerOrder

  theorem 2026-08-13

• cmp_of_sub_inputs_of_balanced

  theorem in IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.IntegerOrder

  theorem 2026-08-13

• gen_pushSimplex_comp_sdOp

  lemma in IndisputableMonolith.Foundation.SingularSubdivision

  lemma 2026-08-13

• self_le_abs

  theorem in IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.IntegerOrder

  theorem 2026-08-13

• recip_num_cmp_zero_of_not_balanced_zero

  theorem in IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.IntegerOrder

  theorem 2026-08-13

• stdSimplex_dist_le_one

  lemma in IndisputableMonolith.Foundation.SingularSubdivision

  lemma 2026-08-13

• twoFaceCert_list_boundary_squared_zero

  theorem in IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.CubicalChainComplex

  theorem 2026-08-13

• abs_mul

  theorem in IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.IntegerOrder

  theorem 2026-08-13

• balanced_both_abs_representatives_iff_balanced_zero

  theorem in IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.IntegerOrder

  theorem 2026-08-13

• factorizationGate_of_primitiveLedgerPosting_nonneg

  theorem in IndisputableMonolith.Foundation.LedgerToFactorization

  theorem 2026-08-13

• nonnegative_work_extensive_of_recognition_work_model

  theorem in IndisputableMonolith.Foundation.UnifiedForcingChain

  theorem 2026-08-13

• abs_ofOrbit

  theorem in IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.IntegerOrder

  theorem 2026-08-13

• crossEq_zero_iff_num_balanced_zero

  theorem in IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.IntegerOrder

  theorem 2026-08-13

• parallelTwoEdgeFlow_coeff_right

  theorem in IndisputableMonolith.Foundation.CircleWindingChain

  theorem 2026-08-13

• factorizationGate_of_primitiveLedgerPosting_monotone

  theorem in IndisputableMonolith.Foundation.LedgerToFactorization

  theorem 2026-08-13

• abs_negate

  theorem in IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.IntegerOrder

  theorem 2026-08-13

• negativeFlag_sub_self

  theorem in IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.IntegerOrder

  theorem 2026-08-13

• shift_plus

  def in IndisputableMonolith.Foundation.ContinuumLimit

  def 2026-08-13

• finite_two_face_ledger_square_zero

  theorem in IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.CubicalChainComplex

  theorem 2026-08-13

• forcedQuotientRecognitionCost

  def in IndisputableMonolith.Foundation.DistinctionToT4

  def 2026-08-13

• abs_sub_self_eq_zero

  theorem in IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.IntegerOrder

  theorem 2026-08-13

• IndisputableMonolith.Foundation.UncertaintyPrinciple3Deep

  module guide in IndisputableMonolith.Foundation.UncertaintyPrinciple3Deep

  module 2026-08-13

• mul_balanced_zero_iff

  theorem in IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.IntegerOrder

  theorem 2026-08-13

• canonical_seed_size_law_of_seed_recognition_work

  theorem in IndisputableMonolith.Foundation.UnifiedForcingChain

  theorem 2026-08-13

• ateeIter_zero

  lemma in IndisputableMonolith.Foundation.SingularSubdivision

  lemma 2026-08-13

• PRCJCostDistanceThreeLegModulusTarget_proved

  theorem in IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.RealCompleteness

  theorem 2026-08-13

• Independent

  def in IndisputableMonolith.Foundation.MaximalForcing.Primitive

  def 2026-08-13

• sdOpIter_zero

  lemma in IndisputableMonolith.Foundation.SingularSubdivision

  lemma 2026-08-13

• RealityClaim

  structure in IndisputableMonolith.Foundation.MaximalForcing.Primitive

  structure 2026-08-13

• PRCNullDistanceTransitiveTarget

  def in IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.RealCauchy

  def 2026-08-13

• selfReference

  def in IndisputableMonolith.Foundation.SeamClosure.Reference

  def 2026-08-13

• evalHom

  def in IndisputableMonolith.Foundation.SeamClosure.Reference

  def 2026-08-13

• ForcedIntegersCert

  structure in IndisputableMonolith.Foundation.UniversalForcing.ForcedIntegers

  structure 2026-08-13

• admissibleOrbit_canonical_base_ratio_phi

  theorem in IndisputableMonolith.Foundation.UnifiedForcingChain

  theorem 2026-08-13

• validComparison_iff_native

  theorem in IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.ValidComparison

  theorem 2026-08-13

• distinction_T0_T2_to_T3

  theorem in IndisputableMonolith.Foundation.DistinctionToT4

  theorem 2026-08-13

• IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.ValidComparisonExamples

  module guide in IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.ValidComparisonExamples

  module 2026-08-13

• factorizationGate_of_ledgerLinearResponse

  theorem in IndisputableMonolith.Foundation.LedgerToFactorization

  theorem 2026-08-13

• cmp_zero_sub_right

  theorem in IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.IntegerOrder

  theorem 2026-08-13

• cmp_sub_zero_right

  theorem in IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.IntegerOrder

  theorem 2026-08-13

• IntegerOrderCertificate

  structure in IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.IntegerOrder

  structure 2026-08-13

• SelectionPrinciple

  structure in IndisputableMonolith.Foundation.MaximalForcing.Primitive

  structure 2026-08-13

• rcl_seed_posting_surface

  theorem in IndisputableMonolith.Foundation.UnifiedForcingChain

  theorem 2026-08-13

• stdSimplex_map_eq_affineMap

  lemma in IndisputableMonolith.Foundation.SingularSubdivision

  lemma 2026-08-13

• cert

  def in IndisputableMonolith.Foundation.RS_Forcing_Chain_Module_009

  def 2026-08-13

• cmp_sub_zero_left

  theorem in IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.IntegerOrder

  theorem 2026-08-13

• cmp_zero_sub_left

  theorem in IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.IntegerOrder

  theorem 2026-08-13

• d2

  def in IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.MultiDistinctionGeometry

  def 2026-08-13

• IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.IntegerOrder

  module guide in IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.IntegerOrder

  module 2026-08-13

• IndisputableMonolith.Foundation.MaximalForcing.AdmissibleRealization

  module guide in IndisputableMonolith.Foundation.MaximalForcing.AdmissibleRealization

  module 2026-08-13

• IndisputableMonolith.Foundation.RS_Forcing_Chain_Module_010

  module guide in IndisputableMonolith.Foundation.RS_Forcing_Chain_Module_010

  module 2026-08-13

• IndisputableMonolith.Foundation.UniversalForcing.ForcedIntegers

  module guide in IndisputableMonolith.Foundation.UniversalForcing.ForcedIntegers

  module 2026-08-13

• IndisputableMonolith.Foundation.MaximalForcing.RealityClosure

  module guide in IndisputableMonolith.Foundation.MaximalForcing.RealityClosure

  module 2026-08-13

• IndisputableMonolith.Gravity.MasterTheoremDeeperPartial

  module guide in IndisputableMonolith.Gravity.MasterTheoremDeeperPartial

  module 2026-08-13

• boundary_squared_zero

  theorem in IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.MultiDistinctionGeometry

  theorem 2026-08-13

• IndisputableMonolith.Foundation.MaximalForcing.Primitive

  module guide in IndisputableMonolith.Foundation.MaximalForcing.Primitive

  module 2026-08-13

• IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.MultiDistinctionGeometry

  module guide in IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.MultiDistinctionGeometry

  module 2026-08-13

• SeedEventSupportModel

  structure in IndisputableMonolith.Foundation.UnifiedForcingChain

  structure 2026-08-13

• canonicalBaseRatio_eq_phi_of_uniformClosed_seed

  theorem in IndisputableMonolith.Foundation.UnifiedForcingChain

  theorem 2026-08-13

• CanonicalSeedPostingOperation

  structure in IndisputableMonolith.Foundation.UnifiedForcingChain

  structure 2026-08-13

• IndisputableMonolith.Cosmology.EarlyUniverse

  module guide in IndisputableMonolith.Cosmology.EarlyUniverse

  module 2026-08-13

• canonical_seed_post_index_unique

  theorem in IndisputableMonolith.Foundation.UnifiedForcingChain

  theorem 2026-08-13

• ratio_reference_zero_iff

  theorem in IndisputableMonolith.Foundation.Reference

  theorem 2026-08-13

• uniform_scale_ratio_unique

  theorem in IndisputableMonolith.Foundation.UnifiedForcingChain

  theorem 2026-08-13

• RSForcingChain002Cert

  structure in IndisputableMonolith.Foundation.RS_Forcing_Chain_Module_002

  structure 2026-08-13

• absValueGeneratedNativeCost

  def in IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.PRCNativeCostUniqueness

  def 2026-08-13

• IndisputableMonolith.Foundation.LedgerToFactorization

  module guide in IndisputableMonolith.Foundation.LedgerToFactorization

  module 2026-08-13

• PRCPrimeCalibratedTwoPrimeReciprocalIdentityNonTwoCompositeDefectCharacter_of_cost_defect

  theorem in IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.PRCNativeCostUniqueness

  theorem 2026-08-13

• windingChainMap_freeToChain_orientedChain

  theorem in IndisputableMonolith.Foundation.CircleWindingChain

  theorem 2026-08-13

• IndisputableMonolith.Foundation.BornRuleForcing

  module guide in IndisputableMonolith.Foundation.BornRuleForcing

  module 2026-08-13

• PeriodWitness

  structure in IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.Factorization.PeriodSpectrum

  structure 2026-08-13

• PRCPrimeCalibrationForcesNonunitOrbitOrientationLocalComparableTraceTarget_refuted

  theorem in IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.PRCNativeCostUniqueness

  theorem 2026-08-13

• CycleOperatorCert

  structure in IndisputableMonolith.Foundation.CycleOperator

  structure 2026-08-13

• cert

  def in IndisputableMonolith.Foundation.ForcingChainCompleteness3

  def 2026-08-13

• constantSingularTwoSimplex_face

  theorem in IndisputableMonolith.Foundation.CircleWindingChain

  theorem 2026-08-13

• shiftLinear

  def in IndisputableMonolith.Foundation.RecognitionOperator

  def 2026-08-13

• sectorProject

  def in IndisputableMonolith.Foundation.RecognitionOperator

  def 2026-08-13

• IndisputableMonolith.Verification.Preregistered.Core

  module guide in IndisputableMonolith.Verification.Preregistered.Core

  module 2026-08-13

• RSForcingChain004Cert

  structure in IndisputableMonolith.Foundation.RS_Forcing_Chain_Module_004

  structure 2026-08-13

• count

  def in IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.DeltaProbability

  def 2026-08-13

• EdgeDistinct

  def in IndisputableMonolith.Foundation.T7CycleRealization

  def 2026-08-13

• cmp_sub_self_right

  theorem in IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.IntegerOrder

  theorem 2026-08-13

• PointPrediction

  structure in IndisputableMonolith.Verification.Preregistered.Core

  structure 2026-08-13

• PRCSignedStrengthenedNativeCostSignedAdmissibleCharacterFactorizationTarget_refuted

  theorem in IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.PRCNativeCostMinimality

  theorem 2026-08-13

• zero_cost_perfect_reference

  theorem in IndisputableMonolith.Foundation.Reference

  theorem 2026-08-13

• IndisputableMonolith.Verification.KnobsCount

  module guide in IndisputableMonolith.Verification.KnobsCount

  module 2026-08-13

• toInt_one

  theorem in IndisputableMonolith.Foundation.UniversalForcing.ForcedIntegers

  theorem 2026-08-13

• inputLedger

  def in IndisputableMonolith.Verification.KnobsCount

  def 2026-08-13

• cmp_add_right

  theorem in IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.IntegerOrder

  theorem 2026-08-13

• PRCPrimeCalibrationForcesPrimeIdentityBranchUniformityTarget_refuted

  theorem in IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.PRCNativeCostUniqueness

  theorem 2026-08-13

• simplexEdge

  def in IndisputableMonolith.Foundation.CircleWindingChain

  def 2026-08-13

• IndisputableMonolith.Verification.Preregistered.AlphaInv.Test

  module guide in IndisputableMonolith.Verification.Preregistered.AlphaInv.Test

  module 2026-08-13

• PRCPrimeCalibrationForcesTwoPrimeIdentityTraceConnectedTarget

  def in IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.PRCNativeCostUniqueness

  def 2026-08-13

• cert

  def in IndisputableMonolith.Foundation.RS_Forcing_Chain_Module_005

  def 2026-08-13

• ComplexNormalized

  def in IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.DeltaAmplitude

  def 2026-08-13

• PRCPrimeCalibrationForcesPrimeIdentityWitnessGlobalizesNonunitTarget

  def in IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.PRCNativeCostUniqueness

  def 2026-08-13

• StructuredSector

  structure in IndisputableMonolith.Foundation.RecognitionOperator

  structure 2026-08-13

• IndisputableMonolith.Verification.Exclusivity.DimensionlessForcing

  module guide in IndisputableMonolith.Verification.Exclusivity.DimensionlessForcing

  module 2026-08-13

• TwoFaceCert

  structure in IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.CubicalChainComplex

  structure 2026-08-13

• PRCPrimeCalibrationForcesNonunitOrbitLocalOrientationTarget

  def in IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.PRCNativeCostUniqueness

  def 2026-08-13

• d1

  def in IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.MultiDistinctionGeometry

  def 2026-08-13

• PRCNativeCostCharacterTraceLiftTarget_of_factorization

  theorem in IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.PRCNativeCostUniqueness

  theorem 2026-08-13

• Primitive

  inductive in IndisputableMonolith.Foundation.MaximalForcing.Primitive

  inductive 2026-08-13

• Vtx

  inductive in IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.MultiDistinctionGeometry

  inductive 2026-08-13

• IndisputableMonolith.Foundation.RS_Forcing_Chain_Module_009

  module guide in IndisputableMonolith.Foundation.RS_Forcing_Chain_Module_009

  module 2026-08-13

• IndisputableMonolith.Verification.CPT.WindowIdentifiability

  module guide in IndisputableMonolith.Verification.CPT.WindowIdentifiability

  module 2026-08-13

• PRCNativeCostCharacterRigidityTarget_refuted

  theorem in IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.PRCNativeCostUniqueness

  theorem 2026-08-13

• factorizationGate_of_rationalLedgerPosting

  theorem in IndisputableMonolith.Foundation.LedgerToFactorization

  theorem 2026-08-13

• FullColumnRank

  def in IndisputableMonolith.Verification.CPT.WindowIdentifiability

  def 2026-08-13

• singularTwoChainFreeToChain

  def in IndisputableMonolith.Foundation.CircleWindingChain

  def 2026-08-13

• C0

  abbrev in IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.MultiDistinctionGeometry

  abbrev 2026-08-13

• LedgeredInput

  structure in IndisputableMonolith.Verification.KnobsCount

  structure 2026-08-13

• C1

  abbrev in IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.MultiDistinctionGeometry

  abbrev 2026-08-13

• PrimitiveLedgerPostingSemantics

  structure in IndisputableMonolith.Foundation.LedgerToFactorization

  structure 2026-08-13

• IndisputableMonolith.Foundation.RS_Forcing_Chain_Module_006

  module guide in IndisputableMonolith.Foundation.RS_Forcing_Chain_Module_006

  module 2026-08-13

• IndisputableMonolith.Foundation.RS_Forcing_Chain_Module_012

  module guide in IndisputableMonolith.Foundation.RS_Forcing_Chain_Module_012

  module 2026-08-13

• IndisputableMonolith.Foundation.RS_Forcing_Chain_Module_008

  module guide in IndisputableMonolith.Foundation.RS_Forcing_Chain_Module_008

  module 2026-08-13

• IndisputableMonolith.Foundation.RS_Forcing_Chain_Module_004

  module guide in IndisputableMonolith.Foundation.RS_Forcing_Chain_Module_004

  module 2026-08-13

• PRCZeroCalibratedNativeCostSignedAdmissibleCharacterFactorizationTarget_refuted

  theorem in IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.PRCNativeCostUniqueness

  theorem 2026-08-13

• twoBranchSignal_normalized

  theorem in IndisputableMonolith.Foundation.BornRuleForcing

  theorem 2026-08-13

• IndisputableMonolith.Foundation.RS_Forcing_Chain_Module_007

  module guide in IndisputableMonolith.Foundation.RS_Forcing_Chain_Module_007

  module 2026-08-13

• parallelTwoEdgeFlow_support

  theorem in IndisputableMonolith.Foundation.CircleWindingChain

  theorem 2026-08-13

• twoThreePrimeMixedDirection

  def in IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.PRCNativeCostUniqueness

  def 2026-08-13

• DimensionSystem

  structure in IndisputableMonolith.Verification.Exclusivity.DimensionlessForcing

  structure 2026-08-13

• const_mem

  theorem in IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.GenerableReal

  theorem 2026-08-13

• sub_zero_balanced

  theorem in IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.IntegerOrder

  theorem 2026-08-13

• PRCPrimeCalibrationForcesTwoPrimeReciprocalForcesPrimeReciprocalTarget_of_split

  theorem in IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.PRCNativeCostUniqueness

  theorem 2026-08-13

• append_extend

  theorem in IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.Basic

  theorem 2026-08-13

• close_to_same_reference

  theorem in IndisputableMonolith.Verification.Exclusivity.PredictionMap

  theorem 2026-08-13

• singularTwoSimplexOfMap

  def in IndisputableMonolith.Foundation.CircleWindingChain

  def 2026-08-13

• ReferentialCapacity

  def in IndisputableMonolith.Foundation.Reference

  def 2026-08-13

• RealizedDefect

  def in IndisputableMonolith.Foundation.T7CycleRealization

  def 2026-08-13

• PRCNativeCostCharacterFactorizationTarget_refuted

  theorem in IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.PRCNativeCostUniqueness

  theorem 2026-08-13

• PerfectReference

  structure in IndisputableMonolith.Foundation.Reference

  structure 2026-08-13

• IsMathematical

  def in IndisputableMonolith.Foundation.Reference

  def 2026-08-13

• shift

  def in IndisputableMonolith.Foundation.ComplexStructureForcing

  def 2026-08-13

• target_of_arcAcyclic

  theorem in IndisputableMonolith.Foundation.PublicSpineLinkingAssembly

  theorem 2026-08-13

• hierarchy_forced_ratio_eq_canonical_base

  theorem in IndisputableMonolith.Foundation.UnifiedForcingChain

  theorem 2026-08-13

• intModuleCat_not_isZero

  theorem in IndisputableMonolith.Foundation.MathlibCohomologyBridge

  theorem 2026-08-13

• allowed_set_A_characterization

  theorem in IndisputableMonolith.Verification.DimensionLinking

  theorem 2026-08-13

• SupportQuotientMap

  structure in IndisputableMonolith.Foundation.UnifiedForcingChain

  structure 2026-08-13

• abs_mul_eq_zero_of_balanced_zero_left

  theorem in IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.IntegerOrder

  theorem 2026-08-13

• ratioReference

  def in IndisputableMonolith.Foundation.Reference

  def 2026-08-13

• prcFormalSystem_exprReflexive

  theorem in IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.PRCDistinctionDichotomy

  theorem 2026-08-13

• lt_sub_zero_right_iff

  theorem in IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.IntegerOrder

  theorem 2026-08-13

• lt_zero_sub_right_iff

  theorem in IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.IntegerOrder

  theorem 2026-08-13

• sub_balanced_zero_iff_of_balanced

  theorem in IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.IntegerOrder

  theorem 2026-08-13

• postComp

  def in IndisputableMonolith.Foundation.SingularSubdivision

  def 2026-08-13

• IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.Continuum.ForcedJOnCompletion

  module guide in IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.Continuum.ForcedJOnCompletion

  module 2026-08-13

• affineMap_idTuple

  lemma in IndisputableMonolith.Foundation.SingularSubdivision

  lemma 2026-08-13

• PerfectSymbol

  structure in IndisputableMonolith.Foundation.Reference

  structure 2026-08-13

• recip_num_balanced_zero_iff

  theorem in IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.IntegerOrder

  theorem 2026-08-13

• IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.ValidComparison

  module guide in IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.ValidComparison

  module 2026-08-13

• simplexEquiv_map

  lemma in IndisputableMonolith.Foundation.SingularSubdivision

  lemma 2026-08-13

• stepReference

  def in IndisputableMonolith.Foundation.SeamClosure.Reference

  def 2026-08-13

• instDecidableBalanced

  instance in IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.IntegerRational

  instance 2026-08-13

• signedOrbitSetoid

  def in IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.IntegerRational

  def 2026-08-13

• toInt_ofInt

  theorem in IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.IntegerRational

  theorem 2026-08-13

• PRCJCostDistanceVerifierTriangleTarget

  def in IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.PRCJCostDistanceTriangle

  def 2026-08-13

• PRCInt

  def in IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.IntegerRational

  def 2026-08-13

• PRCNullDistanceSetoidTarget_of_verifier_triangle

  theorem in IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.PRCJCostDistanceTriangle

  theorem 2026-08-13

• PRCUnitFraction

  def in IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.RealCompleteness

  def 2026-08-13

• pushSimplex

  def in IndisputableMonolith.Foundation.SingularSubdivision

  def 2026-08-13

• PRCNullDistanceSetoidTarget

  def in IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.RealCauchy

  def 2026-08-13

• validComparison_compose

  theorem in IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.ValidComparison

  theorem 2026-08-13

• proj23_apply_coord

  lemma in IndisputableMonolith.Foundation.UnknotComplementRetract

  lemma 2026-08-13

• n_quark_flavours

  def in IndisputableMonolith.Cosmology.GStarDerivation

  def 2026-08-13

• nativeCostSelectionPremiseLedger_all_deltaOnly

  theorem in IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.PRCNativeCostSelection

  theorem 2026-08-13

• T7_from_T8

  theorem in IndisputableMonolith.Foundation.PeriodDependsOnDimension

  theorem 2026-08-13

• omega_lambda_from_phi_carried_prop

  def in IndisputableMonolith.Gravity.MasterTheorem

  def 2026-08-13

• c_RS_observable_distinct

  def in IndisputableMonolith.Gravity.MasterTheorem

  def 2026-08-13

• witness_D5

  theorem in IndisputableMonolith.Verification.DimensionLinking

  theorem 2026-08-13

• shiftLinear_apply

  lemma in IndisputableMonolith.Foundation.RecognitionOperator

  lemma 2026-08-13

• SingularOneSimplex

  abbrev in IndisputableMonolith.Foundation.CircleWindingChain

  abbrev 2026-08-13

• Lorentzian_1_3_proven

  theorem in IndisputableMonolith.Gravity.MasterTheorem

  theorem 2026-08-13

• vertexIndicator

  def in IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.MultiDistinctionGeometry

  def 2026-08-13

• toInt

  def in IndisputableMonolith.Foundation.UniversalForcing.ForcedIntegers

  def 2026-08-13

• forced_difference_fixed_iff

  theorem in IndisputableMonolith.Foundation.UniversalForcing.ForcedIntegers

  theorem 2026-08-13

• constantZeroNativeCost_not_native_hypotheses

  theorem in IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.PRCNativeCostSelection

  theorem 2026-08-13

• realizedClosedScale_canonical_base_ratio_phi

  theorem in IndisputableMonolith.Foundation.UnifiedForcingChain

  theorem 2026-08-13

• realizedHierarchy_canonical_base_ratio_phi

  theorem in IndisputableMonolith.Foundation.UnifiedForcingChain

  theorem 2026-08-13

• t7_t8_to_canonical_schrodinger_bridge_holds

  theorem in IndisputableMonolith.Foundation.UnifiedForcingChain

  theorem 2026-08-13

• mathematics_is_absolute_backbone

  theorem in IndisputableMonolith.Foundation.Reference

  theorem 2026-08-13

• jcost_recip_symmetric

  theorem in IndisputableMonolith.Foundation.UniversalForcing.ReciprocalGenerator

  theorem 2026-08-13

• IsNearMathematical

  def in IndisputableMonolith.Foundation.Reference

  def 2026-08-13

• constants_from_phi

  theorem in IndisputableMonolith.Foundation.UnifiedForcingChain

  theorem 2026-08-13

• discreteReggeCompletionLimit_unique_zero

  theorem in IndisputableMonolith.Foundation.UnifiedForcingChain

  theorem 2026-08-13

• AggregateScalarWorkProjection

  structure in IndisputableMonolith.Foundation.UnifiedForcingChain

  structure 2026-08-13

• uniformClosedMultilevelComposition

  def in IndisputableMonolith.Foundation.UnifiedForcingChain

  def 2026-08-13

• CanonicalGrowthOrientation

  structure in IndisputableMonolith.Foundation.UnifiedForcingChain

  structure 2026-08-13

• incl01

  def in IndisputableMonolith.Foundation.UnknotComplementRetract

  def 2026-08-13

• ultimate_inevitability

  theorem in IndisputableMonolith.Foundation.UnifiedForcingChain

  theorem 2026-08-13

• canonical_growth_iff_ratio_gt_one

  theorem in IndisputableMonolith.Foundation.UnifiedForcingChain

  theorem 2026-08-13

• perfect_reference_cost_zero

  theorem in IndisputableMonolith.Foundation.Reference

  theorem 2026-08-13

• CostSelectionPackageNative

  structure in IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.PRCNativeCostSelection

  structure 2026-08-13

• SequentialReference

  def in IndisputableMonolith.Foundation.Reference

  def 2026-08-13

• same_state_same_outcome

  theorem in IndisputableMonolith.Foundation.MeasurementMechanism

  theorem 2026-08-13

• T0_T8_holds_proven

  theorem in IndisputableMonolith.Gravity.MasterTheorem

  theorem 2026-08-13

• witness_D7

  theorem in IndisputableMonolith.Verification.DimensionLinking

  theorem 2026-08-13

• CanonicalFirstClosureLaw

  structure in IndisputableMonolith.Foundation.UnifiedForcingChain

  structure 2026-08-13

• gauge_generators

  def in IndisputableMonolith.Cosmology.GStarDerivation

  def 2026-08-13

• growthClosedLevels_zero

  theorem in IndisputableMonolith.Foundation.UnifiedForcingChain

  theorem 2026-08-13

• canonical_realized_closed_scale_admissible_orbit_bridge

  theorem in IndisputableMonolith.Foundation.UnifiedForcingChain

  theorem 2026-08-13

• IndisputableMonolith.Physics.QuarkMasses

  module guide in IndisputableMonolith.Physics.QuarkMasses

  module 2026-08-13

• obs_equiv_trans

  theorem in IndisputableMonolith.Foundation.MeasurementMechanism

  theorem 2026-08-13

• t6_to_phi_constants_canonical_bridge_holds

  theorem in IndisputableMonolith.Foundation.UnifiedForcingChain

  theorem 2026-08-13

• continuum_price_residue_wall_tagged

  theorem in IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.PRCNativeCostSelection

  theorem 2026-08-13

• part23_ne_zero

  lemma in IndisputableMonolith.Foundation.UnknotComplementRetract

  lemma 2026-08-13

• support_quotient_compatibility

  theorem in IndisputableMonolith.Foundation.UnifiedForcingChain

  theorem 2026-08-13

• supportQuotientMap_of_support_observation

  theorem in IndisputableMonolith.Foundation.UnifiedForcingChain

  theorem 2026-08-13

• seedClosedLevels

  def in IndisputableMonolith.Foundation.UnifiedForcingChain

  def 2026-08-13

• uniformClosed_after_growthClosed_eq_phiUniform

  theorem in IndisputableMonolith.Foundation.UnifiedForcingChain

  theorem 2026-08-13

• ratio_induced_zero_iff

  theorem in IndisputableMonolith.Foundation.Reference

  theorem 2026-08-13

• periodDimensionBidirectional

  theorem in IndisputableMonolith.Foundation.PeriodDependsOnDimension

  theorem 2026-08-13

• unknot

  def in IndisputableMonolith.Foundation.UnknotComplementRetract

  def 2026-08-13

• ReciprocalGeneratorCert

  structure in IndisputableMonolith.Foundation.UniversalForcing.ReciprocalGenerator

  structure 2026-08-13

• IndisputableMonolith.Cosmology.SphaleronRate

  module guide in IndisputableMonolith.Cosmology.SphaleronRate

  module 2026-08-13

• IndisputableMonolith.Physics.MassResidueNoGo

  module guide in IndisputableMonolith.Physics.MassResidueNoGo

  module 2026-08-13

• SupportQuotientCompatibility

  structure in IndisputableMonolith.Foundation.UnifiedForcingChain

  structure 2026-08-13

• t7_from_t8

  theorem in IndisputableMonolith.Foundation.UnifiedForcingChain

  theorem 2026-08-13

• sectorProject_mode

  lemma in IndisputableMonolith.Foundation.RecognitionOperator

  lemma 2026-08-13

• aggregateScalarWorkProjection_cost

  theorem in IndisputableMonolith.Foundation.UnifiedForcingChain

  theorem 2026-08-13

• ledgerToFloor_surjective

  theorem in IndisputableMonolith.Foundation.LedgerFloorT0Bridge

  theorem 2026-08-13

• canonical_seed_size_law_of_typed_seed_closed

  theorem in IndisputableMonolith.Foundation.UnifiedForcingChain

  theorem 2026-08-13

• FirstNontrivialClosureIndex

  structure in IndisputableMonolith.Foundation.UnifiedForcingChain

  structure 2026-08-13

• t8_triple_route_unique_via_routes

  theorem in IndisputableMonolith.Foundation.UnifiedForcingChain

  theorem 2026-08-13

• canonical_seed_posting_of_operation

  theorem in IndisputableMonolith.Foundation.UnifiedForcingChain

  theorem 2026-08-13

• IndisputableMonolith.Foundation.UniversalForcing.ModularRealization

  module guide in IndisputableMonolith.Foundation.UniversalForcing.ModularRealization

  module 2026-08-13

• routes_AB_agree

  theorem in IndisputableMonolith.Cosmology.EtaBExactRungDerivation

  theorem 2026-08-13

• t5regge_to_continuum_limit_bridge_holds

  theorem in IndisputableMonolith.Foundation.UnifiedForcingChain

  theorem 2026-08-13

• twoAtomSelectionIndex

  def in IndisputableMonolith.Foundation.UnifiedForcingChain

  def 2026-08-13

• gauge_polarisations

  def in IndisputableMonolith.Cosmology.GStarDerivation

  def 2026-08-13

• T8_To_CanonicalSpinor_Bridge

  structure in IndisputableMonolith.Foundation.UnifiedForcingChain

  structure 2026-08-13

• RepresentationEquiv

  def in IndisputableMonolith.Foundation.Reference

  def 2026-08-13

• spine_to_extras_bridge_holds

  theorem in IndisputableMonolith.Foundation.UnifiedForcingChain

  theorem 2026-08-13

• RealizedHierarchyNormalFormEquivalence

  structure in IndisputableMonolith.Foundation.UnifiedForcingChain

  structure 2026-08-13

• g_star_derived_eq_decimal

  theorem in IndisputableMonolith.Cosmology.GStarDerivation

  theorem 2026-08-13

• period_at_D4

  theorem in IndisputableMonolith.Foundation.PeriodDependsOnDimension

  theorem 2026-08-13

• carrier_total

  theorem in IndisputableMonolith.Foundation.GaugeLieCompletionFromCube

  theorem 2026-08-13

• period_eq_eight_iff_D_eq_three

  theorem in IndisputableMonolith.Foundation.PeriodDependsOnDimension

  theorem 2026-08-13

• ClosureNormalFormComposition

  structure in IndisputableMonolith.Foundation.UnifiedForcingChain

  structure 2026-08-13

• recognitionUpdate_eq_shift_on_quarterTurnCore

  theorem in IndisputableMonolith.Foundation.RecognitionOperator

  theorem 2026-08-13

• not_deltaForced_real

  theorem in IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.DeltaForced

  theorem 2026-08-13

• CostUniqueness

  def in IndisputableMonolith.Gravity.MasterTheorem

  def 2026-08-13

• uniformClosedLevels

  def in IndisputableMonolith.Foundation.UnifiedForcingChain

  def 2026-08-13

• T8_DimensionFourRoute_Equivalence

  structure in IndisputableMonolith.Foundation.UnifiedForcingChain

  structure 2026-08-13

• canonical_seed_size_law_of_typed_seed_posting

  theorem in IndisputableMonolith.Foundation.UnifiedForcingChain

  theorem 2026-08-13

• SupportJoinCompatible

  structure in IndisputableMonolith.Foundation.UnifiedForcingChain

  structure 2026-08-13

• fermionic_dof_eq

  theorem in IndisputableMonolith.Cosmology.GStarDerivation

  theorem 2026-08-13

• t5_t7_to_canonical_hamiltonian_bridge_holds

  theorem in IndisputableMonolith.Foundation.UnifiedForcingChain

  theorem 2026-08-13

• distinction_forces_T2

  theorem in IndisputableMonolith.Foundation.DistinctionToT4

  theorem 2026-08-13

• minimalHierarchy_ratio_eq_phi

  theorem in IndisputableMonolith.Foundation.UnifiedForcingChain

  theorem 2026-08-13

• phiUniformClosedLevels_pos

  theorem in IndisputableMonolith.Foundation.UnifiedForcingChain

  theorem 2026-08-13

• canonical_minimal_hierarchy_canonicality

  theorem in IndisputableMonolith.Foundation.UnifiedForcingChain

  theorem 2026-08-13

• realizedClosedScale_canonical_uniform

  theorem in IndisputableMonolith.Foundation.UnifiedForcingChain

  theorem 2026-08-13

• period_at_D2

  theorem in IndisputableMonolith.Foundation.PeriodDependsOnDimension

  theorem 2026-08-13

• IndisputableMonolith.Gravity.QuantumChannel.AmplitudeLinearForcedCert

  module guide in IndisputableMonolith.Gravity.QuantumChannel.AmplitudeLinearForcedCert

  module 2026-08-13

• canonical_support_induced_config_space

  theorem in IndisputableMonolith.Foundation.UnifiedForcingChain

  theorem 2026-08-13

• canonical_uniform_posting_closure_forces_phi

  theorem in IndisputableMonolith.Foundation.UnifiedForcingChain

  theorem 2026-08-13

• channels

  def in IndisputableMonolith.Foundation.RecognitionOperator

  def 2026-08-13

• t5_to_nonlinear_regge_jcost_bridge_holds

  theorem in IndisputableMonolith.Foundation.UnifiedForcingChain

  theorem 2026-08-13

• canonical_growth_closure_preservation

  theorem in IndisputableMonolith.Foundation.UnifiedForcingChain

  theorem 2026-08-13

• MasterTheoremClosureStatus

  structure in IndisputableMonolith.Gravity.MasterTheorem

  structure 2026-08-13

• measurement_creates_correlation

  theorem in IndisputableMonolith.Foundation.MeasurementMechanism

  theorem 2026-08-13

• unknot_isEmbedding

  theorem in IndisputableMonolith.Foundation.UnknotComplementRetract

  theorem 2026-08-13

• RecognitionWorkNonnegativeScaleCompositionModel

  structure in IndisputableMonolith.Foundation.UnifiedForcingChain

  structure 2026-08-13

• T2_FromDistinction

  structure in IndisputableMonolith.Foundation.DistinctionToT4

  structure 2026-08-13

• forcedQuotientBoolEquiv_emp

  theorem in IndisputableMonolith.Foundation.DistinctionToT4

  theorem 2026-08-13

• uniformClosedLevels_eq_original_of_uniform_scale

  theorem in IndisputableMonolith.Foundation.UnifiedForcingChain

  theorem 2026-08-13

• forcedQuotientBoolEquiv

  def in IndisputableMonolith.Foundation.DistinctionToT4

  def 2026-08-13

• falseAtomSupportEvent

  def in IndisputableMonolith.Foundation.UnifiedForcingChain

  def 2026-08-13

• t6_phi_unique_from_derived

  theorem in IndisputableMonolith.Foundation.UnifiedForcingChain

  theorem 2026-08-13

• ledgerToFloor

  def in IndisputableMonolith.Foundation.LedgerFloorT0Bridge

  def 2026-08-13

• canonical_mass_ladder_unique_of_gap_equiv

  theorem in IndisputableMonolith.Foundation.UnifiedForcingChain

  theorem 2026-08-13

• CanonicalSupportQuotientMap

  structure in IndisputableMonolith.Foundation.UnifiedForcingChain

  structure 2026-08-13

• growthClosedLevels_pos

  theorem in IndisputableMonolith.Foundation.UnifiedForcingChain

  theorem 2026-08-13

• PhiUniformClosure

  structure in IndisputableMonolith.Foundation.UnifiedForcingChain

  structure 2026-08-13

• CanonicalSupportObservation

  structure in IndisputableMonolith.Foundation.UnifiedForcingChain

  structure 2026-08-13

• lie_rank_total

  theorem in IndisputableMonolith.Foundation.GaugeLieCompletionFromCube

  theorem 2026-08-13

• fundamental_theorem_of_reference

  theorem in IndisputableMonolith.Foundation.Reference

  theorem 2026-08-13

• IndisputableMonolith.Gravity.LedgerSuperposition

  module guide in IndisputableMonolith.Gravity.LedgerSuperposition

  module 2026-08-13

• costHessianScalar

  def in IndisputableMonolith.Foundation.JHessianGoldenMulti

  def 2026-08-13

• supportEvent_support_disjoint_independence

  theorem in IndisputableMonolith.Foundation.UnifiedForcingChain

  theorem 2026-08-13

• uniformClosedMultilevelComposition_idempotent_levels

  theorem in IndisputableMonolith.Foundation.UnifiedForcingChain

  theorem 2026-08-13

• phiUniformClosedLevels

  def in IndisputableMonolith.Foundation.UnifiedForcingChain

  def 2026-08-13

• supportEvent_support_join_unique

  theorem in IndisputableMonolith.Foundation.UnifiedForcingChain

  theorem 2026-08-13

• supportMap

  def in IndisputableMonolith.Foundation.UnifiedForcingChain

  def 2026-08-13

• SupportJoinCompatibilityCanonicality

  structure in IndisputableMonolith.Foundation.UnifiedForcingChain

  structure 2026-08-13

• witness_p_ge_one

  theorem in IndisputableMonolith.Verification.DimensionLinking

  theorem 2026-08-13

• T6_To_PhiConstants_Canonical_Bridge

  structure in IndisputableMonolith.Foundation.UnifiedForcingChain

  structure 2026-08-13

• mathlibCircleLinkingBackend_of_circleH1MathlibComputation

  theorem in IndisputableMonolith.Foundation.MathlibCohomologyBridge

  theorem 2026-08-13

• RecognitionOperator

  structure in IndisputableMonolith.Foundation.RecognitionOperator

  structure 2026-08-13

• distinction_T1_to_T2

  theorem in IndisputableMonolith.Foundation.DistinctionToT4

  theorem 2026-08-13

• classical_negation_impossible_and_unique_minimizer

  theorem in IndisputableMonolith.Foundation.UnifiedForcingChain

  theorem 2026-08-13

• forcedQuotientConfigSpace

  instance in IndisputableMonolith.Foundation.DistinctionToT4

  instance 2026-08-13

• recipShift_fixed_iff

  theorem in IndisputableMonolith.Foundation.UniversalForcing.ReciprocalGenerator

  theorem 2026-08-13

• DistinctionAtomUniverseFromAbsoluteFloor

  structure in IndisputableMonolith.Foundation.UnifiedForcingChain

  structure 2026-08-13

• phiUniformClosed_levels_unique

  theorem in IndisputableMonolith.Foundation.UnifiedForcingChain

  theorem 2026-08-13

• seedClosedLevels_one

  theorem in IndisputableMonolith.Foundation.UnifiedForcingChain

  theorem 2026-08-13

• canonical_amplitude_normalization

  theorem in IndisputableMonolith.Foundation.UnifiedForcingChain

  theorem 2026-08-13

• canonical_mass_equal_of_rung_gap_equiv

  theorem in IndisputableMonolith.Foundation.UnifiedForcingChain

  theorem 2026-08-13

• canonical_seed_closure_preservation

  theorem in IndisputableMonolith.Foundation.UnifiedForcingChain

  theorem 2026-08-13

• supportCompose

  def in IndisputableMonolith.Foundation.UnifiedForcingChain

  def 2026-08-13

• dft_coefficients_add

  lemma in IndisputableMonolith.Foundation.RecognitionOperator

  lemma 2026-08-13

• cyclicShiftIter_add

  lemma in IndisputableMonolith.Foundation.RecognitionOperator

  lemma 2026-08-13

• canonicalSeedLevelEvent_two

  theorem in IndisputableMonolith.Foundation.UnifiedForcingChain

  theorem 2026-08-13

• supportQuotientEvent_support

  theorem in IndisputableMonolith.Foundation.UnifiedForcingChain

  theorem 2026-08-13

• growthClosedMultilevelComposition_growth

  theorem in IndisputableMonolith.Foundation.UnifiedForcingChain

  theorem 2026-08-13

• T7_To_Realization_Bridge

  structure in IndisputableMonolith.Foundation.UnifiedForcingChain

  structure 2026-08-13

• circleH1ZIsoInt

  def in IndisputableMonolith.Foundation.MathlibCohomologyBridge

  def 2026-08-13

• SupportEvent

  structure in IndisputableMonolith.Foundation.UnifiedForcingChain

  structure 2026-08-13

• supportDisjointIndependence_of_supportQuotient

  theorem in IndisputableMonolith.Foundation.UnifiedForcingChain

  theorem 2026-08-13

• reciprocity_skew

  def in IndisputableMonolith.Foundation.RecognitionOperator

  def 2026-08-13

• cyclicShiftIter_mode

  lemma in IndisputableMonolith.Foundation.RecognitionOperator

  lemma 2026-08-13

• shift_mem_quarterTurnCore

  theorem in IndisputableMonolith.Foundation.RecognitionOperator

  theorem 2026-08-13

• admissibleOrbit_canonical_uniform

  theorem in IndisputableMonolith.Foundation.UnifiedForcingChain

  theorem 2026-08-13

• TypedSeedPostingSemantics

  structure in IndisputableMonolith.Foundation.UnifiedForcingChain

  structure 2026-08-13

• IndisputableMonolith.Gravity.PTAStructural

  module guide in IndisputableMonolith.Gravity.PTAStructural

  module 2026-08-13

• innerForm

  def in IndisputableMonolith.Foundation.JHessianGoldenMulti

  def 2026-08-13

• IndisputableMonolith.Numerics.Interval.Exp

  module guide in IndisputableMonolith.Numerics.Interval.Exp

  module 2026-08-13

• IndisputableMonolith.Foundation.PhiForcingDerived

  module guide in IndisputableMonolith.Foundation.PhiForcingDerived

  module 2026-08-13

• t8_holds

  theorem in IndisputableMonolith.Foundation.UnifiedForcingChain

  theorem 2026-08-13

• twoAtomSelectionIndex_injective

  theorem in IndisputableMonolith.Foundation.UnifiedForcingChain

  theorem 2026-08-13

• constantZeroNativeCost_excluded

  theorem in IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.PRCNativeCostSelection

  theorem 2026-08-13

• MinimalOrbitRealization

  structure in IndisputableMonolith.Foundation.UnifiedForcingChain

  structure 2026-08-13

• IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.TraceClosure

  module guide in IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.TraceClosure

  module 2026-08-13

• is

  structure in IndisputableMonolith.Foundation.UnifiedForcingChain

  structure 2026-08-13

• IndisputableMonolith.Cosmology.PTAStochasticGWStructural

  module guide in IndisputableMonolith.Cosmology.PTAStochasticGWStructural

  module 2026-08-13

• canonical_posting_closure_of_uniform_growth_seed

  theorem in IndisputableMonolith.Foundation.UnifiedForcingChain

  theorem 2026-08-13

• sequential_mediator_optimal

  theorem in IndisputableMonolith.Foundation.Reference

  theorem 2026-08-13

• canonical_support_join_compatibility

  theorem in IndisputableMonolith.Foundation.UnifiedForcingChain

  theorem 2026-08-13

• RecognitionWorkScaleCompositionModel

  structure in IndisputableMonolith.Foundation.UnifiedForcingChain

  structure 2026-08-13

• t7_operator_core_route_equivalence

  theorem in IndisputableMonolith.Foundation.UnifiedForcingChain

  theorem 2026-08-13

• godel_dissolved

  theorem in IndisputableMonolith.Foundation.UnifiedForcingChain

  theorem 2026-08-13

• Symbol

  structure in IndisputableMonolith.Foundation.Reference

  structure 2026-08-13

• composeMorphism

  def in IndisputableMonolith.Foundation.Reference

  def 2026-08-13

• variational_layer_holds

  theorem in IndisputableMonolith.Foundation.UnifiedForcingChain

  theorem 2026-08-13

• T4_To_T5_Cost_Bridge

  structure in IndisputableMonolith.Foundation.UnifiedForcingChain

  structure 2026-08-13

• ProductReference

  def in IndisputableMonolith.Foundation.Reference

  def 2026-08-13

• T6_Phi_Forced

  structure in IndisputableMonolith.Foundation.UnifiedForcingChain

  structure 2026-08-13

• ledgerShadow_eq_true_iff

  theorem in IndisputableMonolith.Foundation.LedgerFloorT0Bridge

  theorem 2026-08-13

• supportFromQuotient

  def in IndisputableMonolith.Foundation.UnifiedForcingChain

  def 2026-08-13

• IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.RealCompletion

  module guide in IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.RealCompletion

  module 2026-08-13

• distinction_atom_universe_from_absolute_floor

  theorem in IndisputableMonolith.Foundation.UnifiedForcingChain

  theorem 2026-08-13

• admissible

  def in IndisputableMonolith.Foundation.RecognitionOperator

  def 2026-08-13

• recip_fixed_iff_cost_zero

  theorem in IndisputableMonolith.Foundation.UniversalForcing.ReciprocalGenerator

  theorem 2026-08-13

• IndisputableMonolith.Physics.MassTopology

  module guide in IndisputableMonolith.Physics.MassTopology

  module 2026-08-13

• IndisputableMonolith.Foundation.PreLogicalCost

  module guide in IndisputableMonolith.Foundation.PreLogicalCost

  module 2026-08-13

• mass_muon_PDG_sigma

  def in IndisputableMonolith.Verification.PDGComparison

  def 2026-08-13

• realizedClosedScale_canonical_seed_size

  theorem in IndisputableMonolith.Foundation.UnifiedForcingChain

  theorem 2026-08-13

• forces_D3_of_arcAcyclic

  theorem in IndisputableMonolith.Foundation.PublicSpineLinkingAssembly

  theorem 2026-08-13

• rat_eq_of

  theorem in IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.DeltaForced

  theorem 2026-08-13

• Variational_To_BornRule_Canonical_Bridge

  structure in IndisputableMonolith.Foundation.UnifiedForcingChain

  structure 2026-08-13

• IndisputableMonolith.Gravity.BlackHoleEntropySI

  module guide in IndisputableMonolith.Gravity.BlackHoleEntropySI

  module 2026-08-13

• IndisputableMonolith.Gravity.DiscriminatorCert

  module guide in IndisputableMonolith.Gravity.DiscriminatorCert

  module 2026-08-13

• retractToCore

  def in IndisputableMonolith.Foundation.UnknotComplementRetract

  def 2026-08-13

• uniform_generator_eq_canonical_base_ratio

  theorem in IndisputableMonolith.Foundation.UnifiedForcingChain

  theorem 2026-08-13

• t6_to_t7_route_equivalence

  theorem in IndisputableMonolith.Foundation.UnifiedForcingChain

  theorem 2026-08-13

• recip

  def in IndisputableMonolith.Foundation.UniversalForcing.ReciprocalGenerator

  def 2026-08-13

• cms_bound_vanishes

  theorem in IndisputableMonolith.Gravity.NonlinearConvergence

  theorem 2026-08-13

• recognition_from_balanced_floor_ledger

  theorem in IndisputableMonolith.Foundation.UnifiedForcingChain

  theorem 2026-08-13

• geodesicOneSimplex_zero_twoPi

  theorem in IndisputableMonolith.Foundation.CircleWindingChain

  theorem 2026-08-13

• T2_Discreteness_Forced

  structure in IndisputableMonolith.Foundation.UnifiedForcingChain

  structure 2026-08-13

• IndisputableMonolith.Numerics.Interval.Basic

  module guide in IndisputableMonolith.Numerics.Interval.Basic

  module 2026-08-13

• fermionic_dof_eq_twice_gap

  theorem in IndisputableMonolith.Unification.FermionDOFGapBridge

  theorem 2026-08-13

• circleH1ZIsoInt_of_cyclicEdgeLists_of_zeroWinding_bounds

  theorem in IndisputableMonolith.Foundation.CircleWindingChain

  theorem 2026-08-13

• pathLift_endpoint_eq_of_winding_zero

  theorem in IndisputableMonolith.Foundation.CircleWinding

  theorem 2026-08-13

• matter_phi45_complementarity

  theorem in IndisputableMonolith.Unification.FermionDOFGapBridge

  theorem 2026-08-13

• boundaryIncidenceSum_zero

  theorem in IndisputableMonolith.Foundation.CircleWindingChain

  theorem 2026-08-13

• IndisputableMonolith.QFT.VacuumFluctuations

  module guide in IndisputableMonolith.QFT.VacuumFluctuations

  module 2026-08-13

• probMass_zero

  theorem in IndisputableMonolith.Foundation.MeasureForcing

  theorem 2026-08-13

• mathlibCircleLinkingBackend_from_circleH1ZNonzero

  def in IndisputableMonolith.Foundation.MathlibCohomologyBridge

  def 2026-08-13

• twoSimplexCoordOneParam_face_two

  theorem in IndisputableMonolith.Foundation.CircleWindingChain

  theorem 2026-08-13

• boolRecognitionCost

  def in IndisputableMonolith.Foundation.UnifiedForcingChain

  def 2026-08-13

• parallelTwoEdgeFlow_ne_zero

  theorem in IndisputableMonolith.Foundation.CircleWindingChain

  theorem 2026-08-13

• reducedCellularCircleChainModelH1IsoInt

  def in IndisputableMonolith.Foundation.CircleH1Computation

  def 2026-08-13

• circleH1ZIsoInt_of_fundamentalCycleClass_generates

  theorem in IndisputableMonolith.Foundation.CircleWindingChain

  theorem 2026-08-13

• vertexBoundaryCoeff_freeMk

  theorem in IndisputableMonolith.Foundation.CircleWindingChain

  theorem 2026-08-13

• singularWinding

  def in IndisputableMonolith.Foundation.CircleWindingChain

  def 2026-08-13

• homologyOneIsoIntOfIsoSingleDegreeOneIntComplex

  def in IndisputableMonolith.Foundation.CircleH1Computation

  def 2026-08-13

• singularEdgePath_zero

  theorem in IndisputableMonolith.Foundation.CircleWindingChain

  theorem 2026-08-13

• geodesicOneSimplex

  def in IndisputableMonolith.Foundation.CircleWindingChain

  def 2026-08-13

• routes_BC_agree

  theorem in IndisputableMonolith.Cosmology.EtaBExactRungDerivation

  theorem 2026-08-13

• UniversalForcingCert

  structure in IndisputableMonolith.Foundation.UniversalForcing

  structure 2026-08-13

• singularOneChainToFree_

  theorem in IndisputableMonolith.Foundation.CircleWindingChain

  theorem 2026-08-13

• cellularCircleAlgebraicH1Certificate

  theorem in IndisputableMonolith.Foundation.CircleH1Computation

  theorem 2026-08-13

• circleH1ZIsoIntOfNonemptyHomotopyEquivOrdinaryCellularAtOne

  theorem in IndisputableMonolith.Foundation.CircleH1Computation

  theorem 2026-08-13

• boundaryIncidenceSum_add

  theorem in IndisputableMonolith.Foundation.CircleWindingChain

  theorem 2026-08-13

• closedSingularOneCycle_boundary_generate_of_rawPrismToFundamental

  theorem in IndisputableMonolith.Foundation.CircleWindingChain

  theorem 2026-08-13

• reducedCellularToOrdinaryChainMap

  def in IndisputableMonolith.Foundation.CircleH1Computation

  def 2026-08-13

• pathDisplacement_homotopic

  theorem in IndisputableMonolith.Foundation.CircleWinding

  theorem 2026-08-13

• detectsNontrivialLinking_three

  theorem in IndisputableMonolith.Foundation.PublicSpine

  theorem 2026-08-13

• ordinaryCellularToReduced_comp_reducedCellularToOrdinary_f_one

  theorem in IndisputableMonolith.Foundation.CircleH1Computation

  theorem 2026-08-13

• absolute_bool_floor_unique_normalized_01

  theorem in IndisputableMonolith.Foundation.UnifiedForcingChain

  theorem 2026-08-13

• largeSupportUniformOrientedExtractionStep

  def in IndisputableMonolith.Foundation.CircleWindingChain

  def 2026-08-13

• geodesicFreeChain_self_bounds

  theorem in IndisputableMonolith.Foundation.CircleWindingChain

  theorem 2026-08-13

• T1_To_T2_Bridge

  structure in IndisputableMonolith.Foundation.UnifiedForcingChain

  structure 2026-08-13

• T0_Logic_Forced

  structure in IndisputableMonolith.Foundation.UnifiedForcingChain

  structure 2026-08-13

• geodesicOneSimplex_shift

  theorem in IndisputableMonolith.Foundation.CircleWindingChain

  theorem 2026-08-13

• DimensionEightTickOpen

  structure in IndisputableMonolith.Foundation.PublicSpine

  structure 2026-08-13

• closedSingularOneCycleList_spans

  def in IndisputableMonolith.Foundation.CircleWindingChain

  def 2026-08-13

• IndisputableMonolith.StandardModel.StrongCP

  module guide in IndisputableMonolith.StandardModel.StrongCP

  module 2026-08-13

• IndisputableMonolith.Unification.FermionDOFGapBridge

  module guide in IndisputableMonolith.Unification.FermionDOFGapBridge

  module 2026-08-13

• circleH1ZNonzero_of_largeSupport_of_zeroWinding_bounds

  theorem in IndisputableMonolith.Foundation.CircleWindingChain

  theorem 2026-08-13

• goldenScalar_forces_phi

  theorem in IndisputableMonolith.Foundation.CostProjectorGolden

  theorem 2026-08-13

• singletonSupportFlow_decomposesIntoCyclicEdgeLists

  theorem in IndisputableMonolith.Foundation.CircleWindingChain

  theorem 2026-08-13

• normalizedProjector_goldenOperator_sq

  theorem in IndisputableMonolith.Foundation.CostProjectorGolden

  theorem 2026-08-13

• zeroFlow_decomposesIntoCyclicEdgeLists

  theorem in IndisputableMonolith.Foundation.CircleWindingChain

  theorem 2026-08-13

• fermi_dirac_weight_D3

  theorem in IndisputableMonolith.Unification.FermionDOFGapBridge

  theorem 2026-08-13

• singularHomologyFunctorSphereOneIntIsoOfQuasiIsoAtOrdinaryCellular

  def in IndisputableMonolith.Foundation.CircleH1Computation

  def 2026-08-13

• linearSingularTwoSimplex

  def in IndisputableMonolith.Foundation.CircleWindingChain

  def 2026-08-13

• windingChainMap_fundamentalCycleFreeChain

  theorem in IndisputableMonolith.Foundation.CircleWindingChain

  theorem 2026-08-13

• ordinaryCellularCircleChainModel

  def in IndisputableMonolith.Foundation.CircleH1Computation

  def 2026-08-13

• freeBoundaryKernel_decomposesIntoDirectedCycles

  def in IndisputableMonolith.Foundation.CircleWindingChain

  def 2026-08-13

• geodesicFreeChain_shift

  theorem in IndisputableMonolith.Foundation.CircleWindingChain

  theorem 2026-08-13

• singularTwoSimplex_boundary_apply

  theorem in IndisputableMonolith.Foundation.CircleWindingChain

  theorem 2026-08-13

• fundamentalCycle_boundary_generates_of_orientedCyclicFamilies

  theorem in IndisputableMonolith.Foundation.CircleWindingChain

  theorem 2026-08-13

• closedSingularOneCycle_zsmul_bounds_of_zero_singularWinding

  theorem in IndisputableMonolith.Foundation.CircleWindingChain

  theorem 2026-08-13

• floorRealizationFromNormalized

  def in IndisputableMonolith.Foundation.UnifiedForcingChain

  def 2026-08-13

• IndisputableMonolith.Foundation.LinkingVanishingLowDim

  module guide in IndisputableMonolith.Foundation.LinkingVanishingLowDim

  module 2026-08-13

• closedSingularOneCycle_bounds_of_raw_boundary

  theorem in IndisputableMonolith.Foundation.CircleWindingChain

  theorem 2026-08-13

• edgeSupportCard_sub_lt_of_supported_exact_cancel

  theorem in IndisputableMonolith.Foundation.CircleWindingChain

  theorem 2026-08-13

• IndisputableMonolith.Physics.ElectronMass.Necessity

  module guide in IndisputableMonolith.Physics.ElectronMass.Necessity

  module 2026-08-13

• trigCirclePoint_surjective

  theorem in IndisputableMonolith.Foundation.CircleWinding

  theorem 2026-08-13

• reversePath

  def in IndisputableMonolith.Foundation.CircleWinding

  def 2026-08-13

• directedCycleExtraction

  theorem in IndisputableMonolith.Foundation.CircleWindingChain

  theorem 2026-08-13

• cycleWinding_integral_of_closedSingularOneCycleList_spans

  theorem in IndisputableMonolith.Foundation.CircleWindingChain

  theorem 2026-08-13

• leptonReprocessingFactor_neg

  theorem in IndisputableMonolith.Cosmology.BaryogenesisStaging

  theorem 2026-08-13

• singularTwoBoundaryFree_freeMk_linearSingularTwoSimplex

  theorem in IndisputableMonolith.Foundation.CircleWindingChain

  theorem 2026-08-13

• IndisputableMonolith.Foundation.CliffordBridge

  module guide in IndisputableMonolith.Foundation.CliffordBridge

  module 2026-08-13

• singularOneChainToFree_freeToChain

  theorem in IndisputableMonolith.Foundation.CircleWindingChain

  theorem 2026-08-12

• boundaryIncidenceSum

  def in IndisputableMonolith.Foundation.CircleWindingChain

  def 2026-08-12

• DetectsNontrivialLinking

  def in IndisputableMonolith.Foundation.PublicSpine

  def 2026-08-12

• sign_unit_ne_zero

  theorem in IndisputableMonolith.Foundation.CircleWindingChain

  theorem 2026-08-12

• continuous_twoSimplexCoordOneParam

  theorem in IndisputableMonolith.Foundation.CircleWindingChain

  theorem 2026-08-12

• IndisputableMonolith.Foundation.QuantumLedger

  module guide in IndisputableMonolith.Foundation.QuantumLedger

  module 2026-08-12

• IndisputableMonolith.Numerics.Interval.Pow

  module guide in IndisputableMonolith.Numerics.Interval.Pow

  module 2026-08-12

• SingularTwoSimplex

  abbrev in IndisputableMonolith.Foundation.CircleWindingChain

  abbrev 2026-08-12

• mathlibCircleLinkingBackend_of_cyclicEdgeLists_of_zeroWinding_bounds

  theorem in IndisputableMonolith.Foundation.CircleWindingChain

  theorem 2026-08-12

• singularHomologyFunctorSphereOneInt_eq_homologyOne

  theorem in IndisputableMonolith.Foundation.CircleH1Computation

  theorem 2026-08-12

• orientedCyclicFamilyTermListChain

  def in IndisputableMonolith.Foundation.CircleWindingChain

  def 2026-08-12

• orientedCyclicFamilies_freePrism_generate_holds

  theorem in IndisputableMonolith.Foundation.CircleWindingChain

  theorem 2026-08-12

• IndisputableMonolith.Foundation.Reference

  module guide in IndisputableMonolith.Foundation.Reference

  module 2026-08-12

• obstruction_Bfinal

  theorem in IndisputableMonolith.Cosmology.BaryogenesisStaging

  theorem 2026-08-12

• edgeInitial

  def in IndisputableMonolith.Foundation.CircleWindingChain

  def 2026-08-12

• t1_holds_eq_routed

  theorem in IndisputableMonolith.Foundation.UnifiedForcingChain

  theorem 2026-08-12

• cost_selection_holds

  theorem in IndisputableMonolith.Foundation.PublicSpine

  theorem 2026-08-12

• circleH1ZIsoInt_of_largeSupport_of_zeroWinding_bounds

  theorem in IndisputableMonolith.Foundation.CircleWindingChain

  theorem 2026-08-12