Encyclopedia Foundation Foundation Primitive Recognition Calculus Delta Native Strong Closure Entry Of

ARTICLE 4 claims 1 theorem 3 models

Foundation Primitive Recognition Calculus Delta Native Strong Closure Entry Of

A named proof entry in a machine-checked certificate of theorems.

Verify this page

The closure entry

Recognition Science keeps a discrete record of events, a ledger, and its framework is built from formal theorems. The declaration entryOf is a small construction in that framework's machine-checked library of formal theorems. It takes two things: a proposition p and a proof h that p holds. It packages them into a ClosureEntry, a named proof entry in the strong closure certificate.

The ClosureEntry structure itself is simple. It has a field closed, which is a proposition, and a field proof, which is a proof of that proposition. So entryOf is a constructor: given any proposition and its proof, it builds a closure entry. This is a definition, not a theorem. It does not assert that any particular proposition is true. It only provides a uniform way to record that a proposition has been proved.

The certificate that uses these entries is the StrongClosureCertificate. It bundles the closed Delta-native theorem surface, meaning it collects the theorems and audit layers of the framework into one object. The theorem delta_native_strong_closure states that such a certificate exists. The certificate itself is assembled by strongClosureCertificate, which is a noncomputable definition.

What entryOf does not claim is important. It does not prove any specific mathematical statement. It does not establish that the framework's theorems are true. It does not even claim that the certificate is complete. It is a packaging device. Its role is organizational: it gives a named, structured way to hold a proof, so that the certificate can point to existing theorem heads. The actual content, the truth of the propositions, comes from the proofs that are passed to it.

In practice, this means entryOf is infrastructure. It is the glue that lets the framework's library assemble a certificate of its closed results. A reader should understand it as a labeled box for a proof, not as a source of mathematical content. The content is in the proofs; the box just carries them.

MODEL entryOf · IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/DeltaNativeStrongClosure.lean
entryOf · IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/DeltaNativeStrongClosure.lean:61 
def entryOf (p : Prop) (h : p) : ClosureEntry := ⟨p, h⟩
MODEL ClosureEntry · IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/DeltaNativeStrongClosure.lean
ClosureEntry · IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/DeltaNativeStrongClosure.lean:56 
/-- A named proof entry in the strong closure certificate. -/
structure ClosureEntry where
  closed : Prop
  proof : closed
THEOREM delta_native_strong_closure · IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/DeltaNativeStrongClosure.lean
delta_native_strong_closure · IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/DeltaNativeStrongClosure.lean:154 
/-- **Delta-native strong closure.** The full Delta-native interface has a single
Lean certificate bundling every closed theorem/audit layer. -/
theorem delta_native_strong_closure : Nonempty StrongClosureCertificate :=
  ⟨strongClosureCertificate⟩
MODEL strongClosureCertificate · IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/DeltaNativeStrongClosure.lean
strongClosureCertificate · IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/DeltaNativeStrongClosure.lean:110 
/-- The concrete certificate assembling the closed Delta-native theorem surface. -/
noncomputable def strongClosureCertificate : StrongClosureCertificate where
  deltaReal := entryOf _ DeltaReal.Protocol.display_real_forgetful
  generableCarrier := fun κ => entryOf _ (GenerableReal.genField_is_operational_carrier κ)
  certifiedAnalytic := fun R =>
    entryOf _ (CertifiedAnalyticProtocols.Expr.transcendental_protocol_closure R)
  certifiedTransformers := fun R =>
    entryOf _ (CertifiedAnalyticTransformers.certified_transformer_headline R)
  frsCarrier := entryOf _ FRSCarrier.frs_carrier
  calibration := entryOf _ DeltaRealCalibration.calibration_gap_closed_by_normalized_interface
  physicalCalibration := entryOf _ PhysicalOneActCalibration.physical_one_act_calibration_headline
  primeAxis := entryOf _ PrimeAxisCoherence.prime_axis_coherence
  multiDistinctionGeometry := entryOf _ MultiDistinctionGeometry.multi_distinction_geometry
  cubicalTwoFace := entryOf _ CubicalChainComplex.finite_two_face_ledger_square_zero
  allDimensionalCubical := entryOf _ AllDimensionalCubicalBoundary.all_dimensional_cubical_boundary_headline
  quotientSelection := fun F => entryOf _ (QuotientSelection.gauge_from_indistinguishability F)
  quotientEmptyExample := entryOf _ QuotientExamples.empty_observable_phase_quotient
  quotientSeparatingExample := entryOf _ QuotientExamples.separating_gauge_family_injective
  quotientProjectiveExample := fun F x y => entryOf _ (QuotientExamples.projective_state_display F x y)
  objecthoodTable := entryOf _ ObjecthoodRegistry.objecthood_periodic_table
  backgroundObjectAudit := entryOf _ ObjecthoodRegistry.background_object_audit
  displayObjectExtension := entryOf _ ObjecthoodRegistry.display_object_extension
  finiteProbability := fun N => entryOf _ (DeltaProbability.delta_probability_headline N)
  finiteAmplitude := fun N => entryOf _ (DeltaAmplitude.delta_amplitude_headline N)
  complexAmplitude := fun N => entryOf _ (DeltaAmplitude.delta_complex_amplitude_headline N)
  frsiAmplitude := fun N => entryOf _ (FRSComplexAmplitude.frsi_amplitude_headline N)
  hilbertDisplay := fun N => entryOf _ (HilbertDisplayCompletion.finite_hilbert_display_headline N)
  physicalComparison := fun B₁ B₂ => entryOf _ (ValidComparison.valid_comparison_doctrine B₁ B₂)
  comparisonExamples := entryOf _ ValidComparisonExamples.valid_comparison_examples_headline
  completionConservativity := fun N D Cert C =>
    entryOf _ (CompletionConservativity.completion_conservativity_headline N D Cert C)
  productCompletion := fun C₁ C₂ P₁ P₂ =>
    entryOf _ (CompletionConservativity.product_completion_headline C₁ C₂ P₁ P₂)
  functionCompletion := fun I {N} {D} {Cert} (C : Completion N D Cert) (P : D → Prop) =>
    entryOf _ (CompletionConservativity.function_completion_headline (I := I) C P)
  finiteCertificateTransfer := fun C P Obstruction hP hO =>
    entryOf _ (FiniteCertificateTransfer.finite_certificate_transfer C P Obstruction hP hO)
  problemAuditReduction := fun A => entryOf _ (QuantizedProofMethod.problemAudit_finiteReduction A)
  stubObligationReflexive := fun s => entryOf _ (show
    QuantizedProofMethod.StubObligation s = QuantizedProofMethod.StubObligation s from rfl)
  hardProblemAudits := entryOf _ HardProblemCertificateAudits.hard_problem_certificate_audits_headline
  certifiedDisplayAudits := entryOf _ HardProblemCertificateAudits.certified_display_audits_headline
  domainSpecificAnalyticAudits := entryOf _ HardProblemCertificateAudits.domain_specific_analytic_audits_headline

What this page does not claim

entryOf does not prove any specific mathematical statement; it only packages a given proof. The existence of a StrongClosureCertificate does not assert that the framework's theorems are true, only that a certificate object exists. The certificate is not claimed to be complete; it bundles the closed theorem surface as defined.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/DeltaNativeStrongClosure.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND