Encyclopedia Foundation Foundation Pair Kernel Canonical Source Green Export S28

ARTICLE 4 claims 4 theorems

Foundation Pair Kernel Canonical Source Green Export S28

A single machine-checked interface bundles several previously separate theorems into one usable input for a physical model.

Verify this page

The unified input surface

Foundation pair kernel canonical source green export s28 is a component in the Recognition Science framework's machine-checked library of formal theorems. Its purpose is practical: it takes several earlier theorem-backed components and bundles them behind one interface, so that a downstream model can treat them as a single input surface. This component introduces no new physical premise. It is a consolidation layer, not a new discovery.

The components it combines come from earlier stages of the framework's development. One is a constructor for posting events, which is the discrete record of occurrences the framework uses as its basic ledger. Another is a signed multiplicity graph that tracks how many times an event occurs, including a repair for a period-two collision where the simpler relation set would record only one occurrence instead of two. Also included are an exact nonlinear first variation, a conserved current, a tangent Hessian, a gauge kernel, and Green attachments. The component also carries a five-class executable-effect carrier with a scale-covariant readout, meaning the readout transforms consistently under changes of scale.

This component establishes that the entire bundle is inhabited: the theorem canonicalSourceGreenExport3 proves that an instance of the structure exists, and the proof is built entirely from the earlier S8 through S27 theorems. In plain terms, the framework proves that all these pieces fit together coherently. The exported native-curvature branch is explicitly a tangent model, and several identifications remain outside the interface: identifying a global field background with the native edge drop, selecting an exact-J field unit, absolute duration or energy units, and identification with an external raw ontology are all not part of what this component claims.

One boundary is worth noting. The exact D+2 exponent survives all duration and energy boundary-unit rescalings, which is a theorem-backed property. But absolute event action is not a function on the full unit quotient; that is an exported boundary, not a missing numerical test. The component also records that period two requires the signed-event multiplicity graph, because the S8 relation set alone would collapse the multiplicity.

What this changes for a reader is the ability to treat a complex stack of theorem-backed components as one object. Instead of tracking each theorem separately, a downstream model can use this single interface, knowing that the framework has already checked that the parts are consistent.

THEOREM canonicalSourceGreenExport3 · IndisputableMonolith/Foundation/PairKernelCanonicalSourceGreenExportS28.lean
canonicalSourceGreenExport3 · IndisputableMonolith/Foundation/PairKernelCanonicalSourceGreenExportS28.lean:225 
/-- The complete export is inhabited entirely by S8-S27 theorems. -/
theorem canonicalSourceGreenExport3 :
    Nonempty CanonicalSourceGreenExport3 := by
  obtain
    ⟨event, hevent, hledgerGreen, hunitTangent,
      hnativeTangent, hnativeScale, hnativeSource, hnotReciprocal⟩ :=
    canonicalExactJTangentConsumer_exists
  refine ⟨{
    event := event
    event_realized := hevent
    event_has_ledger_witness :=
      realizedPrimitivePostingPair_has_ledger_event event hevent
    every_effect_has_event_witness :=
      everyProductionEffectClass_has_realizedEventWitness
    effects_have_physical_instances :=
      executableEffects_have_physicalInstances
    effect_carrier_complete :=
      executableEffectPhysicalCarrier_complete
    effect_carrier_dimension :=
      executableEffectPhysicalCarrier_dimension_eq_five
    no_silent_effect := no_silentProductionEffect
    distinct_effects_are_observable :=
      distinctProductionEffectClasses_have_distinguishingProbe
    exact_action_is_event_fold :=
      recognitionProductionGraph3_exactJCostAction_eq_eventBatch
    signed_support_is_witnessed :=
      signedGraph_support_eq_recognitionGraph_support
    signed_generator_is_framed :=
      pulledBackSignedPostingLaplacian3_eq_framed
    exact_first_variation := by
      intro σ field variation
      exact
        exactJCostAction_hasDerivAt_line_gauss
          (signedRecognitionProductionGraph3 3 σ)
          field variation
    exact_source_is_conserved := by
      intro σ field
      exact
        exactJNonlinearLaplacian_sum_zero
          (signedRecognitionProductionGraph3 3 σ) field
    exact_action_is_gauge_invariant := by
      intro σ field c
      exact
        exactJCostAction_add_const
          (signedRecognitionProductionGraph3 3 σ) field c
    tangent_hessian_is_symmetric := by
      intro σ background left right
      exact
        exactJHessianPairing_comm
          (signedRecognitionProductionGraph3 3 σ)
          background left right
    tangent_hessian_is_nonnegative := by
      intro σ background perturbation
      exact
        exactJHessianAction_nonneg
          (signedRecognitionProductionGraph3 3 σ)
          background perturbation
    tangent_has_gauge_kernel := by
      intro σ background c i
      exact
        exactJTangentLaplacian_const_zero
          (signedRecognitionProductionGraph3 3 σ)
          background c i
    nonlinear_generator_is_frame_invariant :=
      exactJNonlinearLaplacian_signed_frame_independent
    tangent_generator_is_frame_invariant :=
      exactJTangentLaplacian_signed_frame_independent
    ledger_unit_green_attachment := hledgerGreen
    unit_tangent_green_attachment := hunitTangent
    native_curvature_tangent_model := hnativeTangent
    native_tangent_green_scale := hnativeScale
    native_ordered_source_formula := hnativeSource
    native_ordered_source_is_not_reciprocal := hnotReciprocal
    exact_green_ratio_is_scale_covariant :=
      tangentGreenScale_eq_exactJGreenRatio
    raw_external_ontology_remains_independent :=
      externalRawOntology_realization_remains_independent
  }⟩
THEOREM canonicalSourceGreen_forcedExponent · IndisputableMonolith/Foundation/PairKernelCanonicalSourceGreenExportS28.lean
canonicalSourceGreen_forcedExponent · IndisputableMonolith/Foundation/PairKernelCanonicalSourceGreenExportS28.lean:311 
/-- The exact D+2 exponent survives all duration and energy boundary-unit
rescalings. -/
def canonicalSourceGreen_forcedExponent :=
  forcedExponent_survives_unitQuotient
THEOREM canonicalSourceGreen_absoluteActionBoundary · IndisputableMonolith/Foundation/PairKernelCanonicalSourceGreenExportS28.lean
canonicalSourceGreen_absoluteActionBoundary · IndisputableMonolith/Foundation/PairKernelCanonicalSourceGreenExportS28.lean:316 
/-- Absolute event action is not a function on the full unit quotient. This is
an exported boundary, not a missing numerical test. -/
def canonicalSourceGreen_absoluteActionBoundary :=
  absolute_eventAction_not_unit_invariant
THEOREM canonicalSourceGreen_periodTwoCollisionControl · IndisputableMonolith/Foundation/PairKernelCanonicalSourceGreenExportS28.lean
canonicalSourceGreen_periodTwoCollisionControl · IndisputableMonolith/Foundation/PairKernelCanonicalSourceGreenExportS28.lean:321 
/-- Period two requires the signed-event multiplicity graph. The S8 relation
set alone records multiplicity one where the six-slot operator records two. -/
def canonicalSourceGreen_periodTwoCollisionControl :=
  PairKernelPhysicalPostingAttachmentS10.n2_relationSet_collapses_signedDirectionMultiplicity

What this page does not claim

No new physical premise is introduced by this component. The component does not identify a global field background with the native edge drop. The component does not select absolute duration or energy units.

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/PairKernelCanonicalSourceGreenExportS28.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